Termination w.r.t. Q proof of /tmp/tmpYh9Ycd/z30.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(a, f(b, x)))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, x)
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(a, f(b, x))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, x))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))

The TRS R consists of the following rules:

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(a, f(b, x)))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, x)
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(a, f(b, x))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, x))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))

The TRS R consists of the following rules:

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))

The TRS R consists of the following rules:

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
First, we A-transformed [17] the QDP-Problem. Then we obtain the following A-transformed DP problem.
The pairs P are:

a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))

and the Q and R are:
Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))

Q is empty.

By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(a(x₁)) = x₁
POL(a1(x₁)) = x₁
POL(b(x₁)) = x₁

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ UsableRulesReductionPairsProof

            ↳ QDP

              ↳ RFCMatchBoundsDPProof

Q DP problem:
The TRS P consists of the following rules:

a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))

The TRS R consists of the following rules:

a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 2.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))

To find matches we regarded all rules of R and P:

a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

44, 45, 46, 51, 47, 48, 50, 49, 52, 57, 53, 54, 56, 55, 65, 61, 62, 58, 59, 64, 63, 60, 73, 69, 70, 66, 67, 72, 71, 68, 74, 79, 75, 76, 78, 77, 87, 83, 84, 80, 81, 86, 85, 82, 95, 91, 92, 88, 89, 94, 93, 90

Node 44 is start node and node 45 is final node.

Those nodes are connect through the following edges:

44 to 46 labelled a1_1(0)
44 to 50 labelled a1_1(0)
44 to 49 labelled a1_1(0)
44 to 52 labelled a1_1(1)
44 to 56 labelled a1_1(1)
44 to 55 labelled a1_1(1)
44 to 64 labelled a1_1(1)
44 to 63 labelled a1_1(1)
44 to 74 labelled a1_1(2)
44 to 78 labelled a1_1(2)
44 to 77 labelled a1_1(2)
44 to 90 labelled a1_1(2)
44 to 94 labelled a1_1(2)
44 to 82 labelled a1_1(2)
44 to 86 labelled a1_1(2)
44 to 85 labelled a1_1(2)
45 to 45 labelled #_1(0)
46 to 47 labelled a_1(0)
51 to 45 labelled b_1(0)
47 to 48 labelled b_1(0)
48 to 49 labelled a_1(0)
48 to 66 labelled a_1(1)
50 to 51 labelled a_1(0)
49 to 50 labelled a_1(0)
49 to 58 labelled a_1(1)
52 to 53 labelled a_1(1)
57 to 45 labelled b_1(1)
57 to 63 labelled b_1(1)
57 to 60 labelled b_1(1)
57 to 80 labelled b_1(1)
57 to 88 labelled b_1(1)
53 to 54 labelled b_1(1)
54 to 55 labelled a_1(1)
54 to 88 labelled a_1(2)
54 to 80 labelled a_1(2)
56 to 57 labelled a_1(1)
55 to 56 labelled a_1(1)
55 to 58 labelled a_1(1)
65 to 45 labelled b_1(1)
61 to 62 labelled b_1(1)
62 to 63 labelled a_1(1)
62 to 88 labelled a_1(2)
62 to 80 labelled a_1(2)
58 to 59 labelled b_1(1)
59 to 60 labelled a_1(1)
59 to 80 labelled a_1(2)
64 to 65 labelled a_1(1)
63 to 64 labelled a_1(1)
63 to 58 labelled a_1(1)
60 to 61 labelled a_1(1)
73 to 63 labelled b_1(1)
73 to 88 labelled b_1(1)
73 to 80 labelled b_1(1)
69 to 70 labelled b_1(1)
70 to 71 labelled a_1(1)
70 to 88 labelled a_1(2)
70 to 80 labelled a_1(2)
66 to 67 labelled b_1(1)
67 to 68 labelled a_1(1)
67 to 80 labelled a_1(2)
72 to 73 labelled a_1(1)
71 to 72 labelled a_1(1)
71 to 58 labelled a_1(1)
68 to 69 labelled a_1(1)
74 to 75 labelled a_1(2)
79 to 60 labelled b_1(2)
79 to 63 labelled b_1(2)
75 to 76 labelled b_1(2)
76 to 77 labelled a_1(2)
76 to 88 labelled a_1(2)
76 to 80 labelled a_1(2)
78 to 79 labelled a_1(2)
77 to 78 labelled a_1(2)
77 to 58 labelled a_1(1)
87 to 60 labelled b_1(2)
87 to 80 labelled b_1(2)
87 to 88 labelled b_1(2)
83 to 84 labelled b_1(2)
84 to 85 labelled a_1(2)
80 to 81 labelled b_1(2)
81 to 82 labelled a_1(2)
86 to 87 labelled a_1(2)
85 to 86 labelled a_1(2)
82 to 83 labelled a_1(2)
95 to 63 labelled b_1(2)
91 to 92 labelled b_1(2)
92 to 93 labelled a_1(2)
92 to 88 labelled a_1(2)
92 to 80 labelled a_1(2)
88 to 89 labelled b_1(2)
89 to 90 labelled a_1(2)
89 to 80 labelled a_1(2)
94 to 95 labelled a_1(2)
93 to 94 labelled a_1(2)
93 to 58 labelled a_1(1)
90 to 91 labelled a_1(2)